Date: Tue, 07 Jan 1997 15:42:07 GMT
Server: NCSA/1.4.2
Content-type: text/html

<html>
<title>Using Knowledge Automatically</title>
<body    bgcolor="#ffffff"  text="#000000"  link="#0000ee" vlink="551a8b" alink="ff0000">

<h1>Using Knowledge Automatically</h1>

The <em> Bledsoe Philosophy </em> of automated theorem proving is
basically the belief that automated provers must use human-like
methods in order to be successful in mathematics. <p>

When a mathematician tries to prove a theorem, he has the knowledge of
thousands of theorems and definitions.  He also knows how and when to
use them.  This is a very difficult process to automate. <p>

Automatic and semi-automatic theorem proving programs which are able
to use the knowledge of other theorems and definitions are thereby
able to reach arbitrarily far into formalizable mathematics and prove
certain types of theorems.  <p>

The IPR program provides a method for storing and accessing
mathematical knowledge so that an automated theorem proving program
can use it effectively.  We hope this is a step in the right
direction. <p>

The report <!WA0><A
HREF="file://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-127.ps">atp-127.ps</A>
by Benjamin Shults reports on some work in this field.  See the report
<!WA1><a
href="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-127a.ps">atp-127a.ps</a>
for more clear description of the framework without the examples.<P>

Since the publication of those papers, other challenges have appeared.
If you are particularly interested in this work, then ask me about
work in progress.<p>

<hr>

<em>Do you have feedback or want more information?  Contact </em><!WA2><a
href="http://www.ma.utexas.edu/users/bshults">Benjamin Shults</a>.

<hr>

